$\forall$${\it es}$:ES, $x$:Id, $e$:E. $\neg$first($e$) $\Rightarrow$ ($x$ after pred($e$)) $=$ ($x$ when $e$) $\in$ vartype(loc($e$);$x$)